//===-- PTree.cpp ---------------------------------------------------------===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#include "klee/PTree.h"

#include <klee/Expr.h>
#include <klee/util/ExprPPrinter.h>

#include <iostream>
#include <vector>

using namespace klee;

/* *** */

PTree::PTree(const data_type &_root) : root(new Node(0, _root)) {
}

PTree::~PTree() {
}

std::pair<PTreeNode *, PTreeNode *> PTree::split(Node *n, const data_type &leftData, const data_type &rightData) {
    assert(n && !n->left && !n->right);
    assert(n->active && (!n->parent || n->parent->active));
    n->left = new Node(n, leftData);
    n->right = new Node(n, rightData);
    return std::make_pair(n->left, n->right);
}

void PTree::remove(Node *n) {
    assert(!n->left && !n->right);
    deactivate(n);
    do {
        Node *p = n->parent;
        delete n;
        if (p) {
            if (n == p->left) {
                p->left = 0;
            } else {
                assert(n == p->right);
                p->right = 0;
            }
        }
        n = p;
    } while (n && !n->left && !n->right);
}

#if 1
void PTree::deactivate(Node *n) {
    assert(!n->left && !n->right);

    n->active = false;
    n = n->parent;

    while (n) {
        if (n->left && n->right) {
            if (!n->left->active && !n->right->active) {
                n->active = false;
            } else {
                break;
            }
        } else if (!n->left || !n->right) {
            n->active = false;
        } else {
            abort();
        }
        n = n->parent;
    }
}

void PTree::activate(Node *n) {
    assert(!n->left && !n->right);

    while (n) {
        n->active = true;
        n = n->parent;
    }
}
#endif

void PTree::dump(llvm::raw_ostream &os) {
    ExprPPrinter *pp = ExprPPrinter::create(os);
    pp->setNewline("\\l");
    os << "digraph G {\n";
    os << "\tsize=\"10,7.5\";\n";
    os << "\tratio=fill;\n";
    os << "\trotate=90;\n";
    os << "\tcenter = \"true\";\n";
    os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n";
    os << "\tedge [arrowsize=.3]\n";
    std::vector<PTree::Node *> stack;
    stack.push_back(root);
    while (!stack.empty()) {
        PTree::Node *n = stack.back();
        stack.pop_back();
        if (n->condition.isNull()) {
            os << "\tn" << n << " [label=\"\"";
        } else {
            os << "\tn" << n << " [label=\"";
            pp->print(n->condition);
            os << "\",shape=diamond";
        }
        if (n->data)
            os << ",fillcolor=green";
        os << "];\n";
        if (n->left) {
            os << "\tn" << n << " -> n" << n->left << ";\n";
            stack.push_back(n->left);
        }
        if (n->right) {
            os << "\tn" << n << " -> n" << n->right << ";\n";
            stack.push_back(n->right);
        }
    }
    os << "}\n";
    delete pp;
}

PTreeNode::PTreeNode(PTreeNode *_parent, ExecutionState *_data)
    : parent(_parent), left(0), right(0), data(_data), condition(0), active(true) {
}

PTreeNode::~PTreeNode() {
}
